The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2).

0 CpxRelTRS
↳1 RelTrsToTrsProof (UPPER BOUND(ID), 0 ms)
↳2 CpxTRS
↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 2 ms)
↳4 CdtProblem
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
↳6 CdtProblem
↳7 CdtUsableRulesProof (⇔, 0 ms)
↳8 CdtProblem
↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 156 ms)
↳10 CdtProblem
↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 143 ms)
↳12 CdtProblem
↳13 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)
↳14 CdtProblem
↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 191 ms)
↳16 CdtProblem
↳17 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳18 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

isort(Cons(x, xs), r) → isort(xs, insert(x, r))
insert(x', Cons(x, xs)) → insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
isort(Nil, r) → r
insert(x, Nil) → Cons(x, Nil)
inssort(xs) → isort(xs, Nil)

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
insert[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, insert(x', xs))
insert[Ite][False][Ite](True, x, r) → Cons(x, r)

Rewrite Strategy: INNERMOST

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

transformed relative TRS to TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

isort(Cons(x, xs), r) → isort(xs, insert(x, r))
insert(x', Cons(x, xs)) → insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
isort(Nil, r) → r
insert(x, Nil) → Cons(x, Nil)
inssort(xs) → isort(xs, Nil)
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
insert[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, insert(x', xs))
insert[Ite][False][Ite](True, x, r) → Cons(x, r)

Rewrite Strategy: INNERMOST

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

isort(Cons(z0, z1), z2) → isort(z1, insert(z0, z2))
isort(Nil, z0) → z0
insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
insert(z0, Nil) → Cons(z0, Nil)
inssort(z0) → isort(z0, Nil)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2))
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1)
Tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
ISORT(Nil, z0) → c1
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
INSERT(z0, Nil) → c3
INSSORT(z0) → c4(ISORT(z0, Nil))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
<'(0, S(z0)) → c6
<'(z0, 0) → c7
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
INSERT[ITE][FALSE][ITE](True, z0, z1) → c9
S tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
ISORT(Nil, z0) → c1
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
INSERT(z0, Nil) → c3
INSSORT(z0) → c4(ISORT(z0, Nil))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
<'(0, S(z0)) → c6
<'(z0, 0) → c7
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
INSERT[ITE][FALSE][ITE](True, z0, z1) → c9
K tuples:none
Defined Rule Symbols:

isort, insert, inssort, <, insert[Ite][False][Ite]

Defined Pair Symbols:

ISORT, INSERT, INSSORT, <', INSERT[ITE][FALSE][ITE]

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

INSSORT(z0) → c4(ISORT(z0, Nil))
Removed 5 trailing nodes:

<'(z0, 0) → c7
INSERT(z0, Nil) → c3
ISORT(Nil, z0) → c1
<'(0, S(z0)) → c6
INSERT[ITE][FALSE][ITE](True, z0, z1) → c9

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

isort(Cons(z0, z1), z2) → isort(z1, insert(z0, z2))
isort(Nil, z0) → z0
insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
insert(z0, Nil) → Cons(z0, Nil)
inssort(z0) → isort(z0, Nil)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2))
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1)
Tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
S tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
K tuples:none
Defined Rule Symbols:

isort, insert, inssort, <, insert[Ite][False][Ite]

Defined Pair Symbols:

ISORT, INSERT, <', INSERT[ITE][FALSE][ITE]

Compound Symbols:

c, c2, c5, c8

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

isort(Cons(z0, z1), z2) → isort(z1, insert(z0, z2))
isort(Nil, z0) → z0
inssort(z0) → isort(z0, Nil)

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
insert(z0, Nil) → Cons(z0, Nil)
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2))
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
Tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
S tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
K tuples:none
Defined Rule Symbols:

insert, insert[Ite][False][Ite], <

Defined Pair Symbols:

ISORT, INSERT, <', INSERT[ITE][FALSE][ITE]

Compound Symbols:

c, c2, c5, c8

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
We considered the (Usable) Rules:none
And the Tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(<(x1, x2)) = 0   
POL(<'(x1, x2)) = 0   
POL(Cons(x1, x2)) = [1] + x2   
POL(False) = 0   
POL(INSERT(x1, x2)) = 0   
POL(INSERT[ITE][FALSE][ITE](x1, x2, x3)) = 0   
POL(ISORT(x1, x2)) = x1   
POL(Nil) = 0   
POL(S(x1)) = 0   
POL(True) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c2(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c8(x1)) = x1   
POL(insert(x1, x2)) = 0   
POL(insert[Ite][False][Ite](x1, x2, x3)) = 0   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
insert(z0, Nil) → Cons(z0, Nil)
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2))
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
Tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
S tuples:

INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
K tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
Defined Rule Symbols:

insert, insert[Ite][False][Ite], <

Defined Pair Symbols:

ISORT, INSERT, <', INSERT[ITE][FALSE][ITE]

Compound Symbols:

c, c2, c5, c8

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
We considered the (Usable) Rules:

insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2))
insert(z0, Nil) → Cons(z0, Nil)
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1)
And the Tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [2]   
POL(<(x1, x2)) = x1·x2   
POL(<'(x1, x2)) = 0   
POL(Cons(x1, x2)) = [1] + x2   
POL(False) = 0   
POL(INSERT(x1, x2)) = [2]x2   
POL(INSERT[ITE][FALSE][ITE](x1, x2, x3)) = [2]x3   
POL(ISORT(x1, x2)) = [2]x1·x2 + [2]x12   
POL(Nil) = [2]   
POL(S(x1)) = 0   
POL(True) = [1]   
POL(c(x1, x2)) = x1 + x2   
POL(c2(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c8(x1)) = x1   
POL(insert(x1, x2)) = [2] + x2   
POL(insert[Ite][False][Ite](x1, x2, x3)) = [2] + x3   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
insert(z0, Nil) → Cons(z0, Nil)
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2))
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
Tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
S tuples:

INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
K tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
Defined Rule Symbols:

insert, insert[Ite][False][Ite], <

Defined Pair Symbols:

ISORT, INSERT, <', INSERT[ITE][FALSE][ITE]

Compound Symbols:

c, c2, c5, c8

(13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
insert(z0, Nil) → Cons(z0, Nil)
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2))
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
Tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
S tuples:

<'(S(z0), S(z1)) → c5(<'(z0, z1))
K tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
Defined Rule Symbols:

insert, insert[Ite][False][Ite], <

Defined Pair Symbols:

ISORT, INSERT, <', INSERT[ITE][FALSE][ITE]

Compound Symbols:

c, c2, c5, c8

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

<'(S(z0), S(z1)) → c5(<'(z0, z1))
We considered the (Usable) Rules:

insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2))
insert(z0, Nil) → Cons(z0, Nil)
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1)
And the Tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(<(x1, x2)) = 0   
POL(<'(x1, x2)) = x1   
POL(Cons(x1, x2)) = [1] + x1 + x2   
POL(False) = 0   
POL(INSERT(x1, x2)) = [1] + x1 + x1·x2   
POL(INSERT[ITE][FALSE][ITE](x1, x2, x3)) = [1] + x2·x3   
POL(ISORT(x1, x2)) = [2]x1·x2 + [2]x12   
POL(Nil) = 0   
POL(S(x1)) = [1] + x1   
POL(True) = [1]   
POL(c(x1, x2)) = x1 + x2   
POL(c2(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c8(x1)) = x1   
POL(insert(x1, x2)) = [2] + [2]x1 + x2   
POL(insert[Ite][False][Ite](x1, x2, x3)) = [2] + [2]x2 + x3   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2))
insert(z0, Nil) → Cons(z0, Nil)
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2))
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1)
<(S(z0), S(z1)) → <(z0, z1)
<(0, S(z0)) → True
<(z0, 0) → False
Tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
S tuples:none
K tuples:

ISORT(Cons(z0, z1), z2) → c(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c8(INSERT(z0, z2))
INSERT(z0, Cons(z1, z2)) → c2(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
<'(S(z0), S(z1)) → c5(<'(z0, z1))
Defined Rule Symbols:

insert, insert[Ite][False][Ite], <

Defined Pair Symbols:

ISORT, INSERT, <', INSERT[ITE][FALSE][ITE]

Compound Symbols:

c, c2, c5, c8

(17) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(18) BOUNDS(1, 1)